\begin{tabbing}
with declarations 
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]effect of $k$(v) is $x$ := $f$ s v
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=mk{-}ma(${\it ds}$;\+
\\[0ex]${\it da}$;
\\[0ex];
\\[0ex];
\\[0ex]$\langle$$k$$,\,$$x$$\rangle$ : $f$;
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex])
\-
\end{tabbing}